// 
// File:   prism_ir.h
// Author: cionescu
//
// Created on March 21, 2007, 11:21 PM
//

#ifndef _prism_ir_H
#define	_prism_ir_H

#include <map>
#include <vector>
#include <util>
#include <cudd.h>

#include "bdd_manager.h"

/**
The IR data structure is the internal data structure of sqpmc. It basically 
has the same structure as the ast with the exception that all the function 
symbols are resolved and all the expressions are in MTBDD form. This is
useful in order to have a concise representation of the model over which 
a sampling algorithm can be easily be implemented and it holds also additional
information that can be used to generate the model or an abstraction of the 
model directly from it.
*/
using std::vector;
using std::map;
using std::pair;

prism_ir {

  typedef pair<double, DdNode*> transition_type;
  typedef vector<transition_type> transition_set_type;
  typedef pair<DdNode*, transition_set_type> ir_element_type;
  typedef map<DdNode*, transition_set_type> ir_module_type;
  typedef map<string, ir_module_type> ir_type;
  
  bdd_manager manager;
  ir_type model;
  
  // TODO missing information about how to resolve the module composition.
  
  public:
    prism_ir(bdd_manager const& m, prism_ast_program const& p);
    
    ir_type&
    get_ir() {
      return model;
    }
}

#endif	/* _prism_ir_H */

